basic
\\[0ex]Inj($A$;$B$;$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a_{1}$:$A$, $a_{2}$:$A$. ($f$($a_{1}$) = $f$($a_{2}$) $\in$ $B$) $\Rightarrow$ ($a_{1}$ = $a_{2}$ $\in$ $A$)